$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), $x$:$A$, $v$:$B$($x$).
\\[0ex]$\neg$$x$ $\in$ dom($f$) $\Rightarrow$ $x$ : $v$ $\parallel$ $f$